\begin{tabbing}
fifo+send(${\it es}$;$C$;${\it in}$;$m$;${\it req}$;$j$;$i$;$e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]\& es{-}lnk(${\it es}$; $e$) = ${\it in}$($j$) $\in$ IdLnk
\\[0ex]\& ((es{-}tag(${\it es}$; $e$) = $m$ $\in$ Id) $\vee$ (es{-}tag(${\it es}$; $e$) = ${\it req}$ $\in$ Id))
\\[0ex]\& ($i$ $\in$ es{-}val(${\it es}$; $e$).1 $\in$ $C$)
\-
\end{tabbing}